SherbyNet - /page/wikibook/entry.mu

Micron Document

<!DOCTYPE html>

<title>Property Specification Language</title>

</head>

<span id="openzim-page-title" class="mw-page-title-main"><span class="mw-page-title-main">Property Specification Language</span></span>

</h1>

</header>

<p><b>Property Specification Language</b> (<b>PSL</b>) is a <a href="Temporal_logic" title="Temporal logic">temporal logic</a> extending <a href="Linear_temporal_logic" title="Linear temporal logic">linear temporal logic</a> with a range of operators for both ease of expression and enhancement of expressive power. PSL makes an extensive use of <a href="Regular_expressions" class="mw-redirect" title="Regular expressions">regular expressions</a> and syntactic sugaring. It is widely used in the hardware design and verification industry, where <a href="Formal_verification" title="Formal verification">formal verification</a> tools (such as <a href="Model_checking" title="Model checking">model checking</a>) and/or <a href="Logic_simulation" title="Logic simulation">logic simulation</a> tools are used to prove or refute that a given PSL formula holds on a given design.

</p><p>PSL was initially developed by <a href="Accellera" title="Accellera">Accellera</a> for specifying <a href="Property_(philosophy)" title="Property (philosophy)">properties</a> or <a href="Assertion_(computing)" class="mw-redirect" title="Assertion (computing)">assertions</a> about hardware designs. Since September 2004 the <a href="Standardization" title="Standardization">standardization</a> on the language has been done in <a href="IEEE" class="mw-redirect" title="IEEE">IEEE</a> 1850 working group. In September 2005, the IEEE 1850 Standard for Property Specification Language (PSL) was announced.

</p>

<div class="mw-heading mw-heading2"><h2 id="Syntax_and_semantics">Syntax and semantics</h2></div>

<p>PSL can express that if some scenario happens now, then another scenario should happen some time later. For instance, the property "a <style data-mw-deduplicate="TemplateStyles:r886049734">

/* start https://en.wikipedia.org/ */

.mw-parser-output .monospaced{font-family:monospace,monospace}

/* end https://en.wikipedia.org/ */

</style><span class="monospaced">request</span> should always eventually be <span class="monospaced">grant</span>ed" can be expressed by the PSL formula:

</p>

<div class="mw-highlight mw-highlight-lang-text mw-content-ltr" dir="ltr"><pre> always (request -> eventually! grant)

</pre></div>

<p>The property "every <span class="monospaced">request</span> that is immediately followed by an <span class="monospaced">ack</span> signal, should be followed by a complete <span class="monospaced">data transfer</span>, where a complete data transfer is a sequence starting with signal <span class="monospaced">start</span>, ending with signal <span class="monospaced">end</span> in which <span class="monospaced">busy</span> holds at the meantime" can be expressed by the PSL formula:

</p>

<div class="mw-highlight mw-highlight-lang-text mw-content-ltr" dir="ltr"><pre> (true[*]; req; ack) |=> (start; busy[*]; end)

</pre></div>

<p>A trace satisfying this formula is given in the figure on the right.

</p>

<p>PSL's temporal operators can be roughly classified into <i>LTL-style</i> operators and <i>regular-expression-style</i> operators. Many PSL operators come in two versions, a strong version, indicated by an exclamation mark suffix ( <span class="monospaced">!</span> ), and a weak version. The <i>strong version</i> makes eventuality requirements (i.e. require that something will hold in the future), while the <i>weak version</i> does not. An <i>underscore suffix</i> ( <span class="monospaced">_</span> ) is used to differentiate <i>inclusive</i> vs. <i>non-inclusive</i> requirements. The <span class="monospaced">_a</span> and <span class="monospaced">_e</span> suffixes are used to denote <i>universal</i> (all) vs. <i>existential</i> (exists) requirements. Exact time windows are denoted by <span class="monospaced">[n]</span> and flexible by <span class="monospaced">[m..n]</span>.

</p>

<div class="mw-heading mw-heading3"><h3 id="SERE-style_operators">SERE-style operators</h3></div>

<p>The most commonly used PSL operator is the "suffix-implication" operator (also known as the "triggers" operator), which is denoted by <span class="monospaced">|=></span>. Its left operand is a PSL regular expression and its right operand is any PSL formula (be it in LTL style or regular expression style). The semantics of <span class="monospaced">r |=> p</span> is that on every time point i such that the sequence of time points up to i constitute a match to the regular expression r, the path from i+1 should satisfy the property p. This is exemplified in the figures on the right.

</p>

<p>The regular expressions of PSL have the common operators for concatenation (<span class="monospaced">;</span>), Kleene-closure (<span class="monospaced">*</span>), and union (<span class="monospaced">|</span>), as well as operator for fusion (<span class="monospaced">:</span>), intersection (<span class="monospaced">&&</span>) and a weaker version (<span class="monospaced">&</span>), and many variations for consecutive counting <span class="monospaced">[*n]</span> and in-consecutive counting e.g. <span class="monospaced">[=n]</span> and <span class="monospaced">[->n]</span>.

</p><p>The trigger operator comes in several variations, shown in the table below.

</p><p>Here <span class="monospaced">s</span> and <span class="monospaced">t</span> are PSL-regular expressions, and <span class="monospaced">p</span> is a PSL formula.

</p>

<td><div class="mw-highlight mw-highlight-lang-text mw-content-ltr" dir="ltr"><pre> s |=> t!

</pre></div>

</td>

<td>if there is a match of s, then there is a match of t on the suffix of the trace,

<ul><li>t starts the cycle after s ends,</li>

<li>the match of t must reach to its end</li></ul>

</td></tr>

<tr>

<td><div class="mw-highlight mw-highlight-lang-text mw-content-ltr" dir="ltr"><pre> s |-> t!

</pre></div>

</td>

<td>if there is a match of s, then there is a match of t on the suffix of the trace,

<ul><li>t starts the same cycle that s ends,</li>

<li>the match of t must reach to its end</li></ul>

</td></tr>

<tr>

<td><div class="mw-highlight mw-highlight-lang-text mw-content-ltr" dir="ltr"><pre> s |=> t

</pre></div>

</td>

<td>if there is a match of s, then there is a match of t on the suffix of the trace,

<ul><li>t starts the cycle after s ends,</li>

<li>the match of t may "get stuck" in the middle</li></ul>

</td></tr>

<tr>

<td><div class="mw-highlight mw-highlight-lang-text mw-content-ltr" dir="ltr"><pre> s |-> t

</pre></div>

</td>

<td>if there is a match of s, then there is a match of t on the suffix of the trace,

<ul><li>t starts the same cycle that s ends,</li>

<li>the match of t may "get stuck" in the middle</li></ul>

</td></tr>

</tbody></table>

<p>Operators for concatenation, fusion, union, intersection and their variations are shown in the table below.

</p><p>Here <span class="monospaced">s</span> and <span class="monospaced">t</span> are PSL regular expressions.

</p>

</td>

<td>match of s followed by a match of t, t starts the cycle after s ends

</td></tr>

<tr>

</td>

<td>match of s followed by a match of t, t starts the same cycle that s ends

</td></tr>

<tr>

</td>

<td>match of s or match of t

</td></tr>

<tr>

</td>

<td>match of s and match of t, duration of both is of same length

</td></tr>

<tr>

</td>

<td>match of s and match of t, duration matches maybe different

</td></tr>

<tr>

<td><code> s within t </code>

</td>

<td>match of s within a match of t, abbreviation of ([*]; s; [*]) && t

</td></tr>

</tbody></table>

<p>Operators for consecutive repetitions are shown in the table below.

</p><p>Here <span class="monospaced">s</span> is a PSL regular expression.

</p>

</td>

<td>i consecutive repetitions of s

</td></tr>

<tr>

</td>

<td>between i to j consecutive repetitions of s

</td></tr>

<tr>

</td>

<td>at least i to consecutive repetitions of s

</td></tr>

<tr>

</td>

<td>zero or more consecutive repetitions of s

</td></tr>

<tr>

</td>

<td>one or more consecutive repetitions of s

</td></tr>

</tbody></table>

<p>Operators for non-consecutive repetitions are shown in the table below.

</p><p>Here <span class="monospaced">b</span> is any PSL Boolean expression.

</p>

</td>

<td>i not necessarily consecutive repetitions of b,

<ul><li>equivalent to (!b[*];b)[*i]; !b[*]</li></ul>

</td></tr>

<tr>

</td>

<td>at least i and no more than j not necessarily consecutive repetitions of b,

<ul><li>equivalent to (!b[*];b)[*i..j]; !b[*]</li></ul>

</td></tr>

<tr>

</td>

<td>at least i not necessarily consecutive repetitions of b,

<ul><li>equivalent to (!b[*];b)[*i..]; !b[*]</li></ul>

</td></tr>

<tr>

</td>

<td>m not necessarily consecutive repetitions of b ending with b,

<ul><li>equivalent to (!b[*];b)[*m]</li></ul>

</td></tr>

<tr>

</td>

<td>at least m and no more than n not necessarily consecutive repetitions of b ending with b,

<ul><li>equivalent to (!b[*];b)[*m..n]</li></ul>

</td></tr>

<tr>

</td>

<td>at least m not necessarily consecutive repetitions of b ending with b,

<ul><li>equivalent to (!b[*];b)[*m..]; !b[*]</li></ul>

</td></tr>

<tr>

</td>

<td>shortcut for b[->1],

<ul><li>equivalent to (!b[*];b)</li></ul>

</td></tr>

</tbody></table>

<div class="mw-heading mw-heading3"><h3 id="LTL-style_operators">LTL-style operators</h3></div>

<p>Below is a sample of some LTL-style operators of PSL.

</p><p>Here <span class="monospaced">p</span> and <span class="monospaced">q</span> are any PSL formulas.

</p>

<td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">always p</code>

</td>

<td>property p holds on every time point

</td></tr>

<tr>

<td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">never p</code>

</td>

<td>property p does not hold on any time point

</td></tr>

<tr>

<td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">eventually! p</code>

</td>

<td>there exists a future time point where p holds

</td></tr>

<tr>

</td>

<td>there exists a next time point, and p holds on this point

</td></tr>

<tr>

</td>

<td>if there exists a next time point, then p holds on this point

</td></tr>

<tr>

</td>

<td>there exists an n-th time point, and p holds on this point

</td></tr>

<tr>

</td>

<td>if there exists an n-th time point, then p holds on this point

</td></tr>

<tr>

</td>

<td>there exists a time point, within m-th to n-th from the current where p holds.

</td></tr>

<tr>

</td>

<td>if there exists at least n-th time points, then p holds on one of the m-th to n-th points.

</td></tr>

<tr>

</td>

<td>there exists at least n more time points and p holds in all the time points between the m-th to the n-th, inclusive.

</td></tr>

<tr>

</td>

<td>p holds on all the next m-th through n-th time points, however many exist

</td></tr>

<tr>

<td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">p until! q</code>

</td>

<td>there exists a time point where q holds, and p hold up until that time point

</td></tr>

<tr>

<td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">p until q</code>

</td>

<td>p holds up until a time point where q hold, if such exists

</td></tr>

<tr>

<td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">p until!_ q</code>

</td>

<td>there exists a time point where q holds, and p holds up until that time point and in that time point

</td></tr>

<tr>

<td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">p until_ q</code>

</td>

<td>p holds up until a time point where q holds, and in that time point, if such exists

</td></tr>

<tr>

<td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">p before! q</code>

</td>

<td>p holds strictly before the time point where q holds, and p eventually holds

</td></tr>

<tr>

<td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">p before q</code>

</td>

<td>p holds strictly before the time point where q holds, if p never holds, then neither does q

</td></tr>

<tr>

<td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">p before!_ q</code>

</td>

<td>p holds before or at the same time point where q holds, and p eventually holds

</td></tr>

<tr>

<td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">p before_ q</code>

</td>

<td>p holds before or at the same time point where q holds, if p never holds, then neither does q

</td></tr>

</tbody></table>

<div class="mw-heading mw-heading3"><h3 id="Sampling_operator">Sampling operator</h3></div>

<p>Sometimes it is desirable to change the definition of the <i>next time-point</i>, for instance in multiply-clocked designs, or when a higher level of abstraction is desired. The <i>sampling operator</i> (also known as the <i>clock operator</i>), denoted <span class="monospaced">@</span>, is used for this purpose. The formula <span class="monospaced"> p @ c </span> where <span class="monospaced"> p</span> is a PSL formula and <span class="monospaced">c</span> a PSL Boolean expressions holds on a given path if <span class="monospaced"> p</span> on that path projected on the cycles in which <span class="monospaced"> c</span> holds, as exemplified in the figures to the right.

</p>

<p>The first property states that "every <span class="monospaced">request</span> that is immediately followed by an <span class="monospaced">ack</span> signal, should be followed by a complete <span class="monospaced">data transfer</span>, where a complete data transfer is a sequence starting with signal <span class="monospaced">start</span>, ending with signal <span class="monospaced">end</span> in which <span class="monospaced">data</span> should hold at least 8 times:

</p>

<div class="mw-highlight mw-highlight-lang-text mw-content-ltr" dir="ltr"><pre> (true[*]; req; ack) |=> (start; data[=8]; end)

</pre></div>

<p>But sometimes it is desired to consider only the cases where the above signals occur on a cycle where <span class="monospaced">clk</span> is high.

This is depicted in the second figure in which although the formula

</p>

<div class="mw-highlight mw-highlight-lang-text mw-content-ltr" dir="ltr"><pre> ((true[*]; req; ack) |=> (start; data[*3]; end)) @ clk

</pre></div>

<p>uses <span class="monospaced">data[*3]</span> and <span class="monospaced">[*n]</span> is consecutive repetition, the matching trace has 3 non-consecutive time points where <span class="monospaced">data</span> holds, but when considering only the time points where <span class="monospaced">clk</span> holds, the time points where <span class="monospaced">data</span> hold become consecutive.

</p>

<p>The semantics of formulas with nested @ is a little subtle. The interested reader is referred to [2].

</p>

<div class="mw-heading mw-heading3"><h3 id="Abort_operators">Abort operators</h3></div>

<p>PSL has several operators to deal with truncated paths (finite paths that may correspond to a prefix of the computation). Truncated paths occur in bounded-model checking, due to resets and in many other scenarios. The abort operators, specify how eventualities should be dealt with when a path has been truncated. They rely on the truncated semantics proposed in [1].

</p><p>Here <span class="monospaced">p</span> is any PSL formula and <span class="monospaced">b</span> is any PSL Boolean expression.

</p>

<td><code> p async_abort b </code>

</td>

<td>either p holds or p does not fail up until b holds;

<ul><li>b recognized asynchronously</li></ul>

</td></tr>

<tr>

<td><code> p sync_abort b </code>

</td>

<td>either p holds or p does not fail up until b holds;

<ul><li>b recognized synchronously</li></ul>

</td></tr>

<tr>

<td><code> p abort b </code>

</td>

<td>equivalent to p async_abort b

</td></tr>

</tbody></table>

<div class="mw-heading mw-heading3"><h3 id="Expressive_power">Expressive power</h3></div>

<p>PSL subsumes the temporal logic <a href="Linear_temporal_logic" title="Linear temporal logic">LTL</a> and extends its expressive power to that of the <a href="Omega-regular_languages" class="mw-redirect" title="Omega-regular languages">omega-regular languages</a>. The augmentation in expressive power, compared to that of LTL, which has the expressive power of the star-free ω-regular expressions, can be attributed to the <i>suffix implication</i>, also known as the <i>triggers</i> operator, denoted "|->". The formula <i>r |-> f</i> where <i>r</i> is a regular expression and <i>f</i> is a temporal logic formula holds on a computation <i>w</i> if any prefix of <i>w</i> matching <i>r</i> has a continuation satisfying <i>f</i>. Other non-LTL operators of PSL are the <i>@</i> operator, for specifying multiply-clocked designs, the <i>abort</i> operators, for dealing with hardware resets, and <i>local variables</i> for succinctness.

</p>

<div class="mw-heading mw-heading3"><h3 id="Layers">Layers</h3></div>

<p>PSL is defined in 4 layers: the <i>Boolean layer</i>, the <i>temporal layer</i>, the <i>modeling layer</i> and the <i>verification layer</i>.

</p>

<ul><li>The <i>Boolean layer</i> is used for describing a current state of the design and is phrased using one of the above-mentioned HDLs.</li>

<li>The <i>temporal layer</i> consists of the temporal operators used to describe scenarios that span over time (possibly over an unbounded number of time units).</li>

<li>The <i>modeling layer</i> can be used to describe auxiliary state machines in a procedural manner.</li>

<li>The <i>verification layer</i> consists of directives to a verification tool (for instance to <i>assert</i> that a given property is correct or to <i>assume</i> that a certain set of properties is correct when verifying another set of properties).</li></ul>

<div class="mw-heading mw-heading3"><h3 id="Language_compatibility">Language compatibility</h3></div>

<p>Property Specification Language can be used with multiple electronic system design languages (HDLs) such as:

</p>

<li><a href="Verilog" title="Verilog">Verilog</a> (IEEE 1364)</li>

<li><a href="SystemVerilog" title="SystemVerilog">SystemVerilog</a> (IEEE 1800)</li>

<li><a href="SystemC" title="SystemC">SystemC</a> (IEEE 1666) by <a href="Open_SystemC_Initiative" class="mw-redirect" title="Open SystemC Initiative">Open SystemC Initiative (OSCI)</a>.</li></ul>

<p>When PSL is used in conjunction with one of the above HDLs, its Boolean layer uses the operators of the respective HDL.

</p>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite class="citation book cs1"><i>1850-2005 – IEEE Standard for Property Specification Language (PSL)</i>. 2005. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2FIEEESTD.2005.97780">10.1109/IEEESTD.2005.97780</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-7381-4780-X</bdi>.</cite>

<ul><li>IEC 62531:2007 <cite class="citation book cs1"><i>62531-2007 – IEC 62531 Ed. 1 (2007-11) (IEEE Std 1850-2005): Standard for Property Specification Language (PSL)</i>. 2007. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2FIEEESTD.2007.4408637">10.1109/IEEESTD.2007.4408637</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-7381-5727-6</bdi>.</cite></li></ul></li>

<li><cite class="citation book cs1"><i>1850-2010 – IEEE Standard for Property Specification Language (PSL)</i>. 2010. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2FIEEESTD.2010.5446004">10.1109/IEEESTD.2010.5446004</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-7381-6255-3</bdi>.</cite>

<ul><li>IEC 62531:2012 <cite class="citation book cs1"><i>62531-2012 – IEC 62531:2012(E) (IEEE Std 1850-2010): Standard for Property Specification Language (PSL)</i>. 2012. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2FIEEESTD.2012.6228486">10.1109/IEEESTD.2012.6228486</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-7381-7299-6</bdi>.</cite></li></ul></li>

<li><cite id="CITEREFEisnerFismanHavlicekLustig2003" class="citation book cs1">Eisner, Cindy; <a href="Dana_Fisman" title="Dana Fisman">Fisman, Dana</a>; Havlicek, John; Lustig, Yoad; McIsaac, Anthony; Van Campenhout, David (2003). <a rel="nofollow" class="external text" href="http://www.research.ibm.com/people/e/eisner/papers/cav49.pdf">"Reasoning with Temporal Logic on Truncated Paths"</a> <span class="cs1-format">(PDF)</span>. <i><a href="Computer_Aided_Verification" title="Computer Aided Verification">Computer Aided Verification</a></i>. Lecture Notes in Computer Science. Vol. 2725. p. 27. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-540-45069-6_3">10.1007/978-3-540-45069-6_3</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3-540-40524-5</bdi>.</cite></li>

<li><cite id="CITEREFEisnerFismanHavlicekMcIsaac2003" class="citation book cs1">Eisner, Cindy; <a href="Dana_Fisman" title="Dana Fisman">Fisman, Dana</a>; Havlicek, John; McIsaac, Anthony; Van Campenhout, David (2003). <a rel="nofollow" class="external text" href="http://www.cis.upenn.edu/~fisman/documents/EFHMV_ICALP03_full.pdf">"The Definition of a Temporal Clock Operator"</a> <span class="cs1-format">(PDF)</span>. <i>Automata, Languages and Programming</i>. Lecture Notes in Computer Science. Vol. 2719. p. 857. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F3-540-45061-0_67">10.1007/3-540-45061-0_67</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3-540-40493-4</bdi>.</cite></li></ul>

<div class="mw-heading mw-heading2"><h2 id="External_links">External links</h2></div>

<ul><li><a rel="nofollow" class="external text" href="http://www.eda.org/ieee-1850">IEEE 1850 working group</a></li>

<li><a rel="nofollow" class="external text" href="https://web.archive.org/web/20051210035642/http://standards.ieee.org/announcements/pr_1850psl.html">IEEE Announcement September 2005</a></li>

<li><a rel="nofollow" class="external text" href="http://www.accellera.org/">Accellera</a></li>

<li><a rel="nofollow" class="external text" href="http://www.project-veripage.com/psl_tutorial_1.php">Property Specification Language Tutorial</a></li>

<li><a rel="nofollow" class="external text" href="http://www.doulos.com/knowhow/psl/">Designers guide to PSL</a></li></ul>

<div class="mw-heading mw-heading3"><h3 id="Books_on_PSL">Books on PSL</h3></div>

<ul><li><a rel="nofollow" class="external text" href="http://www.systemverilog.us/psl_info.html">Using PSL/Sugar for Formal and Dynamic Verification 2nd Edition, Ben Cohen, Ajeetha Kumari, Srinivasan Venkataramanan</a></li>

<li><a rel="nofollow" class="external text" href="https://www.springer.com/engineering/circuits+%26+systems/book/978-0-387-35313-5">A Practical Introduction to PSL</a>, Cindy Eisner and <a href="Dana_Fisman" title="Dana Fisman">Dana Fisman</a></li></ul>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hlist dl,.mw-parser-output .hlist ol,.mw-parser-output .hlist ul{margin:0;padding:0}.mw-parser-output .hlist dd,.mw-parser-output .hlist dt,.mw-parser-output .hlist li{margin:0;display:inline}.mw-parser-output .hlist.inline,.mw-parser-output .hlist.inline dl,.mw-parser-output .hlist.inline ol,.mw-parser-output .hlist.inline ul,.mw-parser-output .hlist dl dl,.mw-parser-output .hlist dl ol,.mw-parser-output .hlist dl ul,.mw-parser-output .hlist ol dl,.mw-parser-output .hlist ol ol,.mw-parser-output .hlist ol ul,.mw-parser-output .hlist ul dl,.mw-parser-output .hlist ul ol,.mw-parser-output .hlist ul ul{display:inline}.mw-parser-output .hlist .mw-empty-li{display:none}.mw-parser-output .hlist dt::after{content:": "}.mw-parser-output .hlist dd::after,.mw-parser-output .hlist li::after{content:" · ";font-weight:bold}.mw-parser-output .hlist dd:last-child::after,.mw-parser-output .hlist dt:last-child::after,.mw-parser-output .hlist li:last-child::after{content:none}.mw-parser-output .hlist dd dd:first-child::before,.mw-parser-output .hlist dd dt:first-child::before,.mw-parser-output .hlist dd li:first-child::before,.mw-parser-output .hlist dt dd:first-child::before,.mw-parser-output .hlist dt dt:first-child::before,.mw-parser-output .hlist dt li:first-child::before,.mw-parser-output .hlist li dd:first-child::before,.mw-parser-output .hlist li dt:first-child::before,.mw-parser-output .hlist li li:first-child::before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child::after,.mw-parser-output .hlist dd dt:last-child::after,.mw-parser-output .hlist dd li:last-child::after,.mw-parser-output .hlist dt dd:last-child::after,.mw-parser-output .hlist dt dt:last-child::after,.mw-parser-output .hlist dt li:last-child::after,.mw-parser-output .hlist li dd:last-child::after,.mw-parser-output .hlist li dt:last-child::after,.mw-parser-output .hlist li li:last-child::after{content:")";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li::before{content:" "counter(listitem)"\a0 "}.mw-parser-output .hlist dd ol>li:first-child::before,.mw-parser-output .hlist dt ol>li:first-child::before,.mw-parser-output .hlist li ol>li:first-child::before{content:" ("counter(listitem)"\a0 "}

/* end https://en.wikipedia.org/ */

</style><style data-mw-deduplicate="TemplateStyles:r1236075235">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbox{box-sizing:border-box;border:1px solid #a2a9b1;width:100%;clear:both;font-size:88%;text-align:center;padding:1px;margin:1em auto 0}.mw-parser-output .navbox .navbox{margin-top:0}.mw-parser-output .navbox+.navbox,.mw-parser-output .navbox+.navbox-styles+.navbox{margin-top:-1px}.mw-parser-output .navbox-inner,.mw-parser-output .navbox-subgroup{width:100%}.mw-parser-output .navbox-group,.mw-parser-output .navbox-title,.mw-parser-output .navbox-abovebelow{padding:0.25em 1em;line-height:1.5em;text-align:center}.mw-parser-output .navbox-group{white-space:nowrap;text-align:right}.mw-parser-output .navbox,.mw-parser-output .navbox-subgroup{background-color:#fdfdfd}.mw-parser-output .navbox-list{line-height:1.5em;border-color:#fdfdfd}.mw-parser-output .navbox-list-with-group{text-align:left;border-left-width:2px;border-left-style:solid}.mw-parser-output tr+tr>.navbox-abovebelow,.mw-parser-output tr+tr>.navbox-group,.mw-parser-output tr+tr>.navbox-image,.mw-parser-output tr+tr>.navbox-list{border-top:2px solid #fdfdfd}.mw-parser-output .navbox-title{background-color:#ccf}.mw-parser-output .navbox-abovebelow,.mw-parser-output .navbox-group,.mw-parser-output .navbox-subgroup .navbox-title{background-color:#ddf}.mw-parser-output .navbox-subgroup .navbox-group,.mw-parser-output .navbox-subgroup .navbox-abovebelow{background-color:#e6e6ff}.mw-parser-output .navbox-even{background-color:#f7f7f7}.mw-parser-output .navbox-odd{background-color:transparent}.mw-parser-output .navbox .hlist td dl,.mw-parser-output .navbox .hlist td ol,.mw-parser-output .navbox .hlist td ul,.mw-parser-output .navbox td.hlist dl,.mw-parser-output .navbox td.hlist ol,.mw-parser-output .navbox td.hlist ul{padding:0.125em 0}.mw-parser-output .navbox .navbar{display:block;font-size:100%}.mw-parser-output .navbox-title .navbar{float:left;text-align:left;margin-right:0.5em}body.skin--responsive .mw-parser-output .navbox-image img{max-width:none!important}@media print{body.ns-0 .mw-parser-output .navbox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style></div><div role="navigation" class="navbox" aria-labelledby="Programmable_logic116" style="padding:3px"><table class="nowraplinks mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><style data-mw-deduplicate="TemplateStyles:r1239400231">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbar{display:inline;font-size:88%;font-weight:normal}.mw-parser-output .navbar-collapse{float:left;text-align:left}.mw-parser-output .navbar-boxtext{word-spacing:0}.mw-parser-output .navbar ul{display:inline-block;white-space:nowrap;line-height:inherit}.mw-parser-output .navbar-brackets::before{margin-right:-0.125em;content:"[ "}.mw-parser-output .navbar-brackets::after{margin-left:-0.125em;content:" ]"}.mw-parser-output .navbar li{word-spacing:-0.125em}.mw-parser-output .navbar a>span,.mw-parser-output .navbar a>abbr{text-decoration:inherit}.mw-parser-output .navbar-mini abbr{font-variant:small-caps;border-bottom:none;text-decoration:none;cursor:inherit}.mw-parser-output .navbar-ct-full{font-size:114%;margin:0 7em}.mw-parser-output .navbar-ct-mini{font-size:114%;margin:0 4em}html.skin-theme-clientpref-night .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}@media(prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}}@media print{.mw-parser-output .navbar{display:none!important}}

/* end https://en.wikipedia.org/ */

</style><div id="Programmable_logic116" style="font-size:114%;margin:0 4em"><a href="Programmable_logic_device" title="Programmable logic device">Programmable logic</a></div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">Concepts</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Logic_block" title="Logic block">Logic block</a></li></ul></li>

<li><a href="Reconfigurable_computing" title="Reconfigurable computing">Reconfigurable computing</a>

<ul><li><a href="Xputer" title="Xputer">Xputer</a></li></ul></li>

<li><a href="Soft_microprocessor" title="Soft microprocessor">Soft microprocessor</a></li>

<li><a href="Circuit_underutilization" title="Circuit underutilization">Circuit underutilization</a></li>

<li><a href="High-level_synthesis" title="High-level synthesis">High-level synthesis</a></li>

<li><a href="Hardware_acceleration" title="Hardware acceleration">Hardware acceleration</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Hardware_description_language" title="Hardware description language">Languages</a></th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Verilog" title="Verilog">Verilog</a>

<li><a href="VHDL-VITAL" class="mw-redirect" title="VHDL-VITAL">VITAL</a></li></ul></li>

<li><a href="SystemVerilog" title="SystemVerilog">SystemVerilog</a>

<li><a href="SystemC" title="SystemC">SystemC</a></li>

<li><a href="Handel-C" title="Handel-C">Handel-C</a></li>

<li><a href="PALASM" title="PALASM">PALASM</a></li>

<li><a href="MyHDL" title="MyHDL">MyHDL</a></li>

<li><a href="Chisel_(programming_language)" title="Chisel (programming language)">Chisel</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Companies</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Accellera" title="Accellera">Accellera</a></li>

<li><a href="Achronix" title="Achronix">Achronix</a></li>

<li><a href="Aldec" title="Aldec">Aldec</a></li>

<li><a href="Cadence_Design_Systems" title="Cadence Design Systems">Cadence</a></li>

<li><a href="Infineon_Technologies" title="Infineon Technologies">Infineon</a></li>

<li><a href="Intel" title="Intel">Intel</a></li>

<li><a href="Lattice_Semiconductor" title="Lattice Semiconductor">Lattice</a></li>

<li><a href="Microchip_Technology" title="Microchip Technology">Microchip Technology</a></li>

<li><a href="Siemens" title="Siemens">Siemens</a></li>

<li><a href="Synopsys" title="Synopsys">Synopsys</a></li>

<li><a href="Texas_Instruments" title="Texas Instruments">Texas Instruments</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Products</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%">Hardware</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<li><a href="Stratix" title="Stratix">Stratix</a></li>

<li><a href="Virtex_(FPGA)" title="Virtex (FPGA)">Virtex</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Software</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Intel_Quartus_Prime" class="mw-redirect" title="Intel Quartus Prime">Intel Quartus Prime</a></li>

<li><a href="Xilinx_ISE" title="Xilinx ISE">Xilinx ISE</a></li>

<li><a href="Vivado" title="Vivado">Vivado</a></li>

<li><a href="ModelSim" title="ModelSim">ModelSim</a></li>

<li><a href="List_of_HDL_simulators" title="List of HDL simulators">Simulators</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Intellectual_property" title="Intellectual property">Intellectual<br>property</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Proprietary_hardware" title="Proprietary hardware">Proprietary</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<li><a href="ARM_Cortex-M" title="ARM Cortex-M">ARM Cortex-M</a></li>

<li><a href="LatticeMico8" title="LatticeMico8">LatticeMico8</a></li>

<li><a href="MicroBlaze" title="MicroBlaze">MicroBlaze</a></li>

<li><a href="PicoBlaze" title="PicoBlaze">PicoBlaze</a></li>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Open-source_hardware" title="Open-source hardware">Open-source</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<li><a href="LatticeMico32" title="LatticeMico32">LatticeMico32</a></li>

<li><a href="OpenCores" title="OpenCores">OpenCores</a></li>

<li><a href="OpenRISC" title="OpenRISC">OpenRISC</a>

<li><a href="Power_ISA" title="Power ISA">Power ISA</a>

<ul><li><a href="Libre-SOC" title="Libre-SOC">Libre-SOC</a></li>

<li><a href="OpenPOWER_Microwatt" title="OpenPOWER Microwatt">Microwatt</a></li></ul></li>

</div></td></tr></tbody></table><div></div></td></tr></tbody></table><div></div></td></tr></tbody></table></div>

<div class="navbox-styles"></div><div role="navigation" class="navbox" aria-labelledby="IEEE_standards209" style="padding:3px"><table class="nowraplinks hlist mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><div id="IEEE_standards209" style="font-size:114%;margin:0 4em"><a href="IEEE_Standards_Association" title="IEEE Standards Association">IEEE standards</a></div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">Current</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="IEEE_754-2008_revision" title="IEEE 754-2008 revision">Revision</a></li></ul></li>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="IEEE_802" title="IEEE 802">802 series</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%"><a href="IEEE_802" title="IEEE 802">802</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="WiMAX" title="WiMAX">WiMAX · d · e</a></li></ul></li>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="IEEE_802.1" title="IEEE 802.1">802.1</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="IEEE_802.3" title="IEEE 802.3">802.3</a> <br>(<a href="Ethernet" title="Ethernet">Ethernet</a>)</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="IEEE_802.11" title="IEEE 802.11">802.11</a> <br>(<a href="Wi-Fi" title="Wi-Fi">Wi-Fi</a>)</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<li><a href="IEEE_802.11_(legacy_mode)" title="IEEE 802.11 (legacy mode)">legacy mode</a></li>

<li><a href="IEEE_802.11ad" title="IEEE 802.11ad">ad</a> (<a href="WiGig" title="WiGig">WiGig</a>)</li>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="IEEE_802.15" title="IEEE 802.15">802.15</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="IEEE_802.15.1" class="mw-redirect" title="IEEE 802.15.1">.1</a> (<a href="Bluetooth" title="Bluetooth">Bluetooth</a>)</li>

<li><a href="IEEE_802.15.4" title="IEEE 802.15.4">.4</a> (<a href="Zigbee" title="Zigbee">Zigbee</a>)</li>

</div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Proposed</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Superseded</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

</div></td></tr><tr><td class="navbox-abovebelow" colspan="2"><div>

<ul><li><span class="noviewer" typeof="mw:File"><span title="Category"></span></span> Category</li></ul>

</div></td></tr></tbody></table></div></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2025-08-07" href="https://en.wikipedia.org/wiki/?title=Property_Specification_Language&oldid=1304691075">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>